﻿using System;
using System.Text;
using System.Collections.Generic;
using System.Linq;
using Microsoft.VisualStudio.TestTools.UnitTesting;
using Microsoft.Pex.Framework;


namespace Benchmarks.McMinnThesisBen
{
    /// <summary>
    /// TODO: A complex class. Needs more analysis to understand what is the exact problem
    /// </summary>
    [TestClass]
    public class SlidingWindows
    {
        static int SEND_WINDOW_SIZE = 3;
        static int RECEIVE_WINDOW_SIZE = 3;
        static int  MSG_SIZE = 20;

        // SENDER SIDE STATE
        int sender_seq_no;
        int sender_last_ack_received;
        int sender_last_frame_sent;
        bool[] sent;
        int[][] sender_data;
        // RECEIVER SIDE STATE
        int receiver_next_frame_expected;
        bool[] received;
        int[][] received_data;

        public SlidingWindows()
        {
            sender_seq_no = 0;
            sender_last_ack_received = -1;
            sender_last_frame_sent = -1;
            sent = new bool[SEND_WINDOW_SIZE];
            sender_data = new int[SEND_WINDOW_SIZE][];
            for (int i = 0; i < SEND_WINDOW_SIZE; i++)
            {
                sender_data[i] = new int[MSG_SIZE];
            }
            
            receiver_next_frame_expected = 0;
            received = new bool[RECEIVE_WINDOW_SIZE];
            received_data = new int[RECEIVE_WINDOW_SIZE][];
            for (int i = 0; i < RECEIVE_WINDOW_SIZE; i++)
            {
                sender_data[i] = new int[MSG_SIZE];
            }

        }

        private bool send_window_not_full()
        {
            if ((sender_last_frame_sent - sender_last_ack_received)
                    < SEND_WINDOW_SIZE)
            {
                return true;
            }
            else
            {
                return false;
            }
        }

        private bool is_in_window(int seq_no, int min, int max)
        {
            int pos = seq_no - min;
            int max_pos = max - min + 1;
            if (pos < max_pos)
            {
                return true;
            }
            else
            {
                return false;
            }
        }

        private bool is_next_frame(int seq_no, int next_frame)
        {
            if (seq_no == next_frame)
            {
                return true;
            }
            else
            {
                return false;
            }
        }


        private void send_msg_on_network(int seq_no, int[] data)
        {
        // not implemented
        }

        private void send_ack_on_network(int seq_no)
        {
        // not implemented
        }

        private void deliver_to_application(int[] data)
        {
        // not implemented
        }         

        public void initialise()
        {
            int i;
            for (i = 0; i < SEND_WINDOW_SIZE; i++)
            {
                sent[i] = false;
            }
            for (i = 0; i < RECEIVE_WINDOW_SIZE; i++)
            {
                received[i] = false;
            }
            sender_seq_no = 0;
            sender_last_ack_received = -1;
            sender_last_frame_sent = -1;
            receiver_next_frame_expected = 0;
        }

        public bool send(int[] msg)
        {
            PexAssume.IsTrue(msg.Length == MSG_SIZE);            
            if (send_window_not_full())
            {
                int slot = sender_seq_no % SEND_WINDOW_SIZE;
                sent[slot] = true;
                sender_last_frame_sent ++;
                sender_seq_no ++;
                send_msg_on_network(sender_seq_no, msg);
                return true;
            }
            else
            {
                return false;
            }
        }

        public void receive_ack(int ack_no)
        {
            // sender side
            if (is_in_window(ack_no,
            sender_last_ack_received + 1,
            sender_last_frame_sent))
            {
                while (sender_last_ack_received != ack_no)
                {
                    int slot = (sender_last_ack_received + 1) % SEND_WINDOW_SIZE;
                    sent[slot] = false;
                    sender_last_ack_received++;
                }
            }
        }

        public void receive_frame(int seq_no, int[] data)
        {
            PexAssume.IsTrue(data.Length == MSG_SIZE);    
        
            if (is_in_window(seq_no,
            receiver_next_frame_expected,
            receiver_next_frame_expected + RECEIVE_WINDOW_SIZE - 1))
            {
                int slot = seq_no % RECEIVE_WINDOW_SIZE;
                int i;
                received[slot] = true;
                for (i=0; i < MSG_SIZE; i++)
                {
                    received_data[slot][i] = data[i];
                }
                if (is_next_frame(seq_no, receiver_next_frame_expected))
                {
                    while (received[slot])
                    {
                        deliver_to_application(received_data[slot]);
                        received[slot] = false;
                        receiver_next_frame_expected++;
                        slot = receiver_next_frame_expected % RECEIVE_WINDOW_SIZE;
                        receiver_next_frame_expected++;
                    }
                    send_ack_on_network(seq_no);
                }
            }
            // else ignore frame
        }


        //run with C:\pex\bin\Debug>Pex Benchmarks.dll /mf:TestSlidingWindowsFitness
        // adding /fte outputs all generated tests
        //[PexMethod(MaxRuns = 100, MaxConditions = int.MaxValue, MaxRunsWithoutNewTests = int.MaxValue)]        
        //public void TestSlidingWindowsFitness(
        //                    int[] modifiers, int[] seq_nos, int[][] datalist)
        //{
        //    TestSlidingWindows(modifiers, seq_nos, datalist);
        //}

        //run with C:\pex\bin\Debug>Pex Benchmarks.dll /mf:TestSlidingWindowsDefault
        // adding /fte outputs all generated tests
        //[PexMethod(MaxRuns = 100, MaxConditions = int.MaxValue, MaxRunsWithoutNewTests = int.MaxValue)]
        //public void TestSlidingWindowsDefault(
        //                    int[] modifiers, int[] seq_nos, int[][] datalist)
        //{
        //    TestSlidingWindows(modifiers, seq_nos, datalist);
        //}

        //private void TestSlidingWindows(
        //                    int[] modifiers, int[] seq_nos, int[][] datalist)
        //{
        //    PexAssume.IsTrue(modifiers != null);
        //    PexAssume.IsTrue(seq_nos != null);
        //    PexAssume.IsTrue(datalist != null);
        //    PexAssume.IsTrue(modifiers.Length == seq_nos.Length);
        //    PexAssume.IsTrue(modifiers.Length == datalist.Length);

        //    SlidingWindows c = new SlidingWindows();
        //    for (int i = 0; i <= (modifiers.Length - 1); i++)
        //    {
        //        switch (modifiers[i])
        //        {
        //            case 0:
        //                c.initialise();
        //                break;
        //            case 1:
        //                c.send(datalist[i]);
        //                break;
        //            case 2:
        //                c.receive_ack(seq_nos[i]);
        //                break;
        //            default:
        //                c.receive_frame(seq_nos[i], datalist[i]);
        //                break;
        //        }
        //    }
        //}
    }
}
